\begin{tabbing}
$\forall$\=$A$:Type, ${\it eq}$:EqDecider($A$), ${\it df}$:$x$:$A$ fp$\rightarrow$ Type, $f$:$x$:$A$ fp$\rightarrow$ ${\it df}$($x$)?Top, ${\it dg}$:$x$:$A$ fp$\rightarrow$ Type,\+
\\[0ex]$g$:$x$:$A$ fp$\rightarrow$ ${\it dg}$($x$)?Top.
\-\\[0ex]${\it df}$ $\parallel$ ${\it dg}$
\\[0ex]$\Rightarrow$ ($\forall$$x$:$A$. ($\uparrow$$x$ $\in$ dom($f$)) $\Rightarrow$ ($\uparrow$$x$ $\in$ dom(${\it df}$)))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$A$. ($\uparrow$$x$ $\in$ dom($g$)) $\Rightarrow$ ($\uparrow$$x$ $\in$ dom(${\it dg}$)))
\\[0ex]$\Rightarrow$ ($f$ $\oplus$ $g$ $\in$ $x$:$A$ fp$\rightarrow$ ${\it df}$ $\oplus$ ${\it dg}$($x$)?Top)
\end{tabbing}